Inference at * 1 
Iof proof for Lemma pair eta rw:



1. A : Type
2. B : AType
3. p : a:A  B(a)
  <p.1, p.2> = p 

latex

 by ((D 3) 
CollapseTHEN (AbReduce 0)) 

latex

C1: 

C1: 3. a : A
C1: 4. p1 : B(a)
C1:   <a, p1> = <a, p1>
C.

Definitions

t.2, t.1